COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%axioms for the McCarthy-Painter compiler%
C00004 ENDMK
C⊗;
%axioms for the McCarthy-Painter compiler%

declare INDVAR x x1 x2 x3 y y1 y2 y3 z z1 z2 z3 w w1 w2 w3,
	PREDPAR FI 1,OPCONST a 3 c 2,PREDCONST isvar 1 isstate 1 isnum 1;

axiom
assign:	∀ x w.(isvar(x)∧isstate(w)⊃isnum(c(x,w))),
	∀ x y w.(isvar(x)∧isnum(y)∧isstate(w)⊃isstate(a(x,y,w))),
	∀ x y w.(isvar(x)∧isnum(y)∧isstate(w)⊃c(x,a(x,y,w))=y),
	∀ x1 x2 y w.(isvar(x1)∧isvar(x2)∧isnum(y)∧isstate(w)∧¬(x1=x2)
		⊃c(x2,a(x1,y,w))=c(x2,w)),
	∀ x y1 y2 w.(isvar(x)∧isnum(y1)∧isnum(y2)∧isstate(w)
		⊃ a(x,y2,a(x,y1,w))=a(x,y2,w)),
	∀ x1 x2 y1 y2 w.(isvar(x1)∧isvar(x2)∧isnum(y1)∧isnum(y2)∧¬(x1=x2)
		⊃ a(x2,y2,a(x1,y1,w))=a(x1,y1,a(x2,y2,w))),
	∀ x w.a(x,c(x,w),w)=w;;